Music

Music

Okay

Paul breathing heavily

Crying

So,

so welcome back to AI on this very frosty morning.

We are looking still at agents

who use first order logic as a world description language,

i.e. we are having world models that instead of having states,

we have world descriptions in a description language, first order logic.

And we are basically, we have a knowledge base, phi,

and we want to add knowledge to the model

to the model if phi plus, say, the percepts, let me call them pi,

entail, say, think of a query, is it safe in one-one,

or is there a wumpus or a pit or whatever, so that I can make decisions.

And for this question, we've looked at tableau.

Tableau takes phi, makes them true, pi makes them true,

and the query, label it with false,

saturate at tableau up to a certain multiplicity level

because we know those are unbounded,

and then on every branch see whether we can identify

a set of pairs

that can be unified at the same time.

And the key idea here for first order logic,

where we have to kind of guess instances for variables,

for quantified variables, is that we postpone the decision

of which instances we give for variables to the very end,

to the stage where we have this mating, this set of pairs,

that we want to make the same.

So we're postponing the choice of instances

until we have much more information, namely the information,

I have to make this equal to that and this equal to that and so on,

and this process is called unification.

So if you think about it,

and indeed if you think about first order terms,

now first order formulae,

they are trees obviously, or DAGs, let's think about trees,

and essentially they are the same,

and essentially they look like Mount Fujiyama

or something like this.

It has an ice cap, something like this,

and everything that you see up here is for all, exists,

or and not, all of those things that have to do

with Booleans, with truth values.

And down there we see things like F and G and A and constants,

and on the border here we have the predicates P and Q

and all of those kind of things.

There's a real difference between the ice cap

in terms of semantics.